#include "PDTExpNumBinDerived.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTAdd::PDTAdd(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right) :
  PDTExpNumBin(CG, left, right)
{
}

Z3_ast
PDTAdd::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  Z3_ast args[2];
  Z3NodeVisitHelper(ZV, args);
  Z3node = Z3_mk_add(ZV.ctx, 2, args);
  return Z3node;
}

PDTSubt::PDTSubt(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right) :
  PDTExpNumBin(CG, left, right)
{
}

Z3_ast
PDTSubt::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  Z3_ast args[2];
  Z3NodeVisitHelper(ZV, args);
  Z3node = Z3_mk_sub(ZV.ctx, 2, args);
  return Z3node;
}

PDTMult::PDTMult(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right) :
  PDTExpNumBin(CG, left, right)
{
}

Z3_ast
PDTMult::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  Z3_ast args[2];
  Z3NodeVisitHelper(ZV, args);
  Z3node = Z3_mk_mul(ZV.ctx, 2, args);
  return Z3node;
}

PDTDiv::PDTDiv(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right) :
  PDTExpNumBin(CG, left, right)
{
}

Z3_ast
PDTDiv::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  Z3_ast args[2];
  Z3NodeVisitHelper(ZV, args);
  Z3node = Z3_mk_div(ZV.ctx, args[0], args[1]);
  return Z3node;
}

PDTMod::PDTMod(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right) :
  PDTExpNumBin(CG, left, right)
{
}

Z3_ast
PDTMod::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  Z3_ast args[2];
  Z3NodeVisitHelper(ZV, args);
  Z3node = Z3_mk_mod(ZV.ctx, args[0], args[1]);
  return Z3node;
}
